| Definitions | t  T,  x:A. B(x), E, [e, e'], ES, before(e), es-ble{i:l}(es;e;e'), filter(P;l),  b, xL. P(x), P   Q, False,  A, e  e' , Prop, P  Q, P & Q, P Q, x(s), (x l), (e <loc e'), 1of(t), source(l), destination(l), 2of(t), tag(k), msg(l;t;v), tl(l), i< j, ij, nth_tl(n;as), hd(l), l[i], SWellFounded(R(x;y)), Trans x,y:T. E(x;y), ESAxioms(E;T;M;loc;kind;val;when;after;sends;sender;index;first;pred;causl), outl(x), lnk(k), Y, ||as||, i j < k, {i..j }, isrcv(k), mlnk(m), haslink(l;m), Msg(M), Msg_sub(l;M), isl(x), b, islocal(k), if b t else f fi, kindcase(k; a.f(a); l,t.g(l;t) ), eventtype(k;loc;V;M;e), Knd, Top, IdLnk, AB,  , Id, Unit,  , EqDecider(T), {T}, SQType(T) |